T:Type, a:T, L1, L2:(T List). [a / L1]  L2  L1  L2 

latex

Definitions	x:A. B(x), P  Q, t  T, A, b, null(as), tl(l), ff, if b then t else f fi , False,
Lemmas	sublist transitivity, sublist tl, false wf, sublist wf, sublist weakening